(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
f(S(x'), S(x)) → h(g(x', S(x)), f(S(S(x')), x))
h(0, S(x)) → h(0, x)
h(0, 0) → 0
g(S(x), S(x')) → h(f(S(x), S(x')), g(x, S(S(x'))))
g(S(x), 0) → 0
f(S(x), 0) → 0
h(S(x), x2) → h(x, x2)
g(0, x2) → 0
f(0, x2) → 0
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(2n):
The rewrite sequence
f(S(S(x15_1)), S(x)) →+ h(h(h(g(x15_1, S(x)), f(S(S(x15_1)), x)), g(x15_1, S(S(x)))), f(S(S(S(x15_1))), x))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0,1].
The pumping substitution is [x / S(x)].
The result substitution is [ ].
The rewrite sequence
f(S(S(x15_1)), S(x)) →+ h(h(h(g(x15_1, S(x)), f(S(S(x15_1)), x)), g(x15_1, S(S(x)))), f(S(S(S(x15_1))), x))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [x / S(x)].
The result substitution is [x15_1 / S(x15_1)].
(2) BOUNDS(2^n, INF)